T:Type{i}, x:T, L:T List, P:(TTProp{i'}).
(x,yx.L.P(x,y))  (x,yL.P(x,y)) & (yL. P(x,y)) 

latex

Definitions	Dec(P), P  Q, SQType(T), {T}, l[i], ij, i<j, hd(l), , (x  l), x:A. B(x), A & B, ij, P  Q, P  Q, x,y. t(x;y), x. t(x), Prop, (x,yL.P(x;y)), xL. P(x), i  j < k, AB, P & Q, A, False, P  Q, x(s1,s2), {i..j}, t  T, ||as||, x:A. B(x)
Lemmas	length wf1, int seg wf, l all wf, pairwise wf, le wf, select cons tl sq, non neg length, length cons, l member wf, decidable int equal, select wf, select member